/* Copyright (c) 2011-2012 ISP RAS, Moscow. For more information please write to
 
      mermakov@ispras.ru
      svartanov@ispras.ru

   Licensed under the Apache License, Version 2.0 (the "License");
   you may not use this file except in compliance with the License.
   You may obtain a copy of the License at

       http://www.apache.org/licenses/LICENSE-2.0

   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS,
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
   See the License for the specific language governing permissions and
   limitations under the License.
*/

package ru.ispras.coffeemachine.trace;

import java.io.BufferedReader;
import java.io.IOException;
import java.io.StringReader;
import java.util.ArrayList;
import java.util.List;

import ru.ispras.coffeemachine.util.Logger;

/**
 * Complex queries
 * <ul>
 * <li>True assertions begin with "?1",</li>
 * <li>False assertions begin with "?0",</li>
 * </ul>
 * 
 * @author Sergey Vartanov <me@enzet.ru>
 * @version 1.2.0
 * @since 2011-10-03
 */
public class ComplexQueries
{
	List<String> queries;
	String complexQueries;
	List<Integer> depths;

	public ComplexQueries(String comlexQueries)
	{
		complexQueries = comlexQueries;
		queries = new ArrayList<String>();
		depths = new ArrayList<Integer>();
	}

	/**
	 * Parsing complex queries into set of boolean assertions in STP format
	 * 
	 * @param depth number of assertion that should be inverted
	 */
	public void parse(int depth)
	{
		int currentDepth = 0;

		complexQueries = complexQueries.trim();

		StringReader sr = new StringReader(complexQueries);
		BufferedReader br = new BufferedReader(sr);

		String line;

		String query = "";

		try
		{
			while ((line = br.readLine()) != null)
			{
				line = line.trim();
				
				if (line.length() == 0) {
					continue;
				}
				
				if (line.startsWith("?0"))
				{
					if (currentDepth < depth)
					{
						currentDepth++;
					}
					else
					{
						queries.add(query + "ASSERT(" + line.substring(2) + ");\nQUERY(FALSE);");
						depths.add(++currentDepth);
					}
					query += "ASSERT(NOT(" + line.substring(2) + "));\n";
				}
				else if (line.startsWith("?1"))
				{
					if (currentDepth < depth)
					{
						currentDepth++;
					}
					else
					{
						queries.add(query + "ASSERT(NOT(" + line.substring(2) + "));\nQUERY(FALSE);");
						depths.add(++currentDepth);
					}
					query += "ASSERT(" + line.substring(2) + ");\n";
				}
				else if (line.charAt(0) != '#')
				{
					query += line + "\n";
				}
			}
		}
		catch (IOException e)
		{
			Logger.error("complex queries reading");
		}
	}

	public boolean hasQuery()
	{
		return queries.size() > 0;
	}

	public String getQuery()
	{
		return queries.remove(0);
	}

	public int getDepth()
	{
		return depths.remove(0);
	}

	public int getSize()
	{
		return queries.size();
	}
}
